$\forall$$l$:IdLnk, ${\it dt}$:${\it tg}$:Id fp$\rightarrow$ Type, ${\it knd}$:Knd, $T$:Type.
\\[0ex](isrcv(${\it knd}$) $\Rightarrow$ lnk(${\it knd}$) = $l$ $\Rightarrow$ tag(${\it knd}$) $\in$ dom(${\it dt}$) $\Rightarrow$ $T$ $=$ ${\it dt}$(tag(${\it knd}$)))
\\[0ex]$\Rightarrow$ lnk{-}decl($l$;${\it dt}$) $\parallel$ ${\it knd}$ : $T$